Special features including fairness, concerned with a fair resolution of non-determinism, is often necessary to prove liveness properties. We support several kinds of fairness regrading to event/process levels as well as weak/strong fairness to cater for different requirements. Please refer to our papers [SUNLDP09] for details.

Parallel verification, which makes use of today's popular multi-core architecture of computers, provides efficient approaches to solve problems under sequential algorithms as well as a solution to integrate fairness with existing parallel model checking algorithms. Detailed information are introduced in our paper [LIUSD09].

Verification of Infinite Systems, we use the process abstract counter techniques to group infinitely many similar processes together and check their properties as an abstracted process group, instead of checking satisfiability of each process which makes the problem undecidable. A novel technique for checking such systems under fairness, against Linear Temporal Logic(LTL) formulae is also proposed in our paper that checking properties under fairness is always essential. For detailed information, please refer to [SUNLRLD09].

Verification of Linearizability, linearizability is one of the critical correctness criteria for shared objects. Operations on the shared objects without linearizability may cause system to be inconsistent which will bring in errors even disasters. Existing methods to check linearizability require users to have special knowledge of linearization points and cannot be automatic. We come up a new method to check linearizability based on refinement relations which overcome these drawbacks. Please refer to our paper [LIUWLS09] for details.

All of these topics are parts of our publications.